(set-logic QF_BV)
(declare-fun _substvar_245_ () (_ BitVec 4))
(declare-fun _substvar_261_ () (_ BitVec 25))
(declare-fun _substvar_247_ () (_ BitVec 4))
(declare-fun _substvar_518_ () Bool)
(declare-fun _substvar_582_ () (_ BitVec 21))
(assert (let ( (?v_11 (= _substvar_245_ (_ bv1 4))) (?v_25 ((_ extract 3 0) _substvar_261_))) (and true (and true true true true true ?v_11) true true (= _substvar_261_ (concat _substvar_582_ _substvar_245_)) (ite _substvar_518_ (and true true true true true true (= _substvar_247_ ?v_25)) (and true true true true true true (= (_ bv0 4) ?v_25))) (= (_ bv0 4) (bvor (_ bv0 4) _substvar_247_)) true true true true true true true true true true true true true true true true true true true true true true)))
(check-sat)
(exit)
